{-# LANGUAGE OverlappingInstances, FunctionalDependencies, TypeOperators, TypeFamilies, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances  #-}

import Control.Parallel
import Control.Parallel.Strategies
import Data.List

import Prelude hiding (pred, succ)

import Data.TypeLevel.Num hiding ((+), (-), (*) )

import Model hiding (fa, fb, split, hSplit)

main = do
 print "start..."

 let f  = lift2 (*) fa fb
     xs = replicate 100000 (1:::2:::"String":::3:::4:::Null)

 print $ foldl' (+) 0 $ map f xs

 print $ hMap ToDouble $ head xs
 print $ hFoldr ExtendF (xs !! 0) $ xs !! 0

 let n  =  22
     dn = d22

 print $ "A homogeneous   list : sum [1..n], n = " ++ show n
 print $ sum [0..n]
 print $ "A heterogeneous list : sum [1..n], n = " ++ show n
 print $ hFoldr AddF (0::Int) $ hBetween dn
-- print $ hBetween dn

 print "done."

--

lift :: ( n ~ Length xs , HSplitAt n xy , (xs, ys) ~ SplitAt n xy ) => (a -> b -> c) -> (xs -> a) -> (ys -> b) -> xy -> c
lift f fa fb = split f fa fb undefined
  where
   split :: ( n ~ Length xs , HSplitAt n xy , (xs, ys) ~ SplitAt n xy ) => (a -> b->c) -> (xs -> a) -> (ys -> b) -> Length xs -> xy -> c
   split f fa fb n  = (\(x,y) -> f (fa x) (fb y)) . hSplitAt n

lift2 :: (HSplitAt2 xs ys) => (a -> b -> c) -> (xs -> a) -> (ys -> b) -> Append xs ys -> c
lift2 f fa fb = (\(x,y) -> f (fa x) (fb y)) . hSplitAt2 n
  where
   n = undefined -- :: Length xs

---

fa :: (Int ::: Double ::: Null) -> Double
fa (_ ::: x ::: Null) = x

fb :: (String :::  Int:::Double ::: Null) -> Double
fb (_ ::: _ ::: x ::: Null) = x

--

data ToDouble = ToDouble

instance  HApplay ToDouble Int where
   type Applay ToDouble Int = Int
   applay _ n = n+1

instance  HApplay ToDouble Double where
   type Applay ToDouble Double = Double
   applay _ n = n+1

instance HApplay ToDouble String where
   type Applay ToDouble String = Int
   applay _ s = length s

data ExtendF = ExtendF

instance HApplay ExtendF (x,xs) where
   type Applay ExtendF (x,xs) = x ::: xs
   applay _ (x,xs) = x ::: xs

data AddF = AddF

instance Num x => HApplay AddF (x,x) where
   type Applay AddF (x,x) = x
   applay _ (x,y) = x + y

-- A heterogeneous fold for all types

class (HList xs) => HFoldr f v xs where
  type Foldr f v xs
  hFoldr :: f -> v -> xs -> Foldr f v xs

instance HFoldr f v Null where
  type Foldr f v Null = v
  hFoldr _ v _ = v

instance ( HFoldr f v xs
         , HApplay f (x, Foldr f v xs)
         )
      =>   HFoldr f v (x:::xs) where
  type Foldr f v (x:::xs) = Applay f (x,Foldr f v xs)
  hFoldr f v (x:::xs) = applay f (x, hFoldr f v xs)

-- Turn a heterogeneous list into a homogeneous one

class HToList l e where
  hToList :: l -> [e]

instance HToList Null e  where
  hToList Null = []

instance HToList l e => HToList (e ::: l) e where
  hToList (e ::: l) = e : hToList l

-- HBetween

class (HList l) => HBetween n l | l -> n, n -> l where
  hBetween :: n -> l

instance HBetween D0 (Int:::Null) where
  hBetween n = (toInt n) ::: Null

instance ( Pos n, HBetween (Pred n) xs) => HBetween n (Int:::xs) where
  hBetween n = (toInt n) ::: (hBetween (pred n))